es:ES, ff:FIFO, f2f+:F2F+-decls.
plus-ify{i:l}(es;ff;is_req  ;is_ack ;awaiting ;owes_ack )
 for clients ff.C sends FIFO
 forfrom j to i via (ff.S[j,i],ff.Codes)
 forreceives at i via (ff.R[i],ff.Decodes)
 forequests i,e. loc(e) = i  Id & is_req  (e)[j] 
 are acknowledged by j,i,e. [e: j is_ack  i][j,i] 

latex

Definitions

e c e', t  ...$L, a.f(a) is c< preserving on e.P(e), {T}, P  Q, P  Q, P  Q, [e: i p j], False, Q f P, Q  f P, A c B, t.1, True, T, x(s), x. t(x), [e: i p j], , Top, fifo+property(es;codes;decodes;C;S;R;T;Req;Ack;i;f), x:A. B(x), t  T, P & Q, P  Q, x:A. B(x), f2f+-pred(e',e), plus-ify{i:l}(es;ff;is_req;is_ack;awaiting;owes_ack), A, Dec(P), SqStable(P), for clients C sends FIFO   from j to i via (S[j,i],codes)   receives at i via (R[i],decodes)

Lemmas

f2f+-pred-preserves-order, es-causl irreflexivity, fifoSender-one-one, f2f+-p+-total, or functionality wrt iff, f2f+-p+-equiv-causl, es-causl wf, es-causl transitivity1, snd-it-of-rcv-it, sq stable and, generated-thread-no-joins, rcv-it-of-snd-it, f2f+-pred-alternates, fifoReceiver-caused, generated-thread-properties3, fifoReceiver-properties, fifoReceiver wf, decidable equal Id, decidable cand, decidable snd-it, snd-it wf, es-causle weakening, es-causl transitivity2, fifoSender-causes, f2f+-pred-sub-causl, subtype rel function, decidable rcv-it, sq stable from decidable, causal-order-preserving wf, es-causle wf, antecedent-surjection wf, f2f+-pred wf, f2f+-req-exists, f2f+-pred-field, f2f+-pred-generates-thread, fifoSender-preserves-order, fifoSender-encoding, fifo-FIFO, fifoSender-antecedent, rcv-it wf, es-loc wf, Id wf, fifoDecodes wf, fifoCodes wf, fifoT wf, fifo+property wf, fifoSender wf, fifo+rewrite, event system wf, FIFO wf, F2F+-decls wf, fifoS wf, es-E wf, fifoR wf, fifoC wf, f2f+Owes wf, f2f+Wait wf, f2f+Ack wf, f2f+Req wf, plus-ify wf, f2f+-property